widget: Redraw when font options change
authorMatthias Clasen <mclasen@redhat.com>
Fri, 3 Sep 2021 17:55:39 +0000 (13:55 -0400)
committerMatthias Clasen <mclasen@redhat.com>
Fri, 3 Sep 2021 17:56:29 +0000 (13:56 -0400)
commit26e632e54958e42dcafedd5b26be1cd150eecb4b
tree8cf8d575355338ac26ce6487f6a0b46708fe5147
parent64d2d7074fa59a4f1d261a866b564eb46ed45007
widget: Redraw when font options change

Its the right thing to do, even if it is a rare event.
gtk/gtkwidget.c